r, s:. -(s - r) = (r - s)   

latex

Definitions	P  Q, T, P & Q, P  Q, P  Q, r - s, True, t  T, x:A. B(x), , S  T
Lemmas	qadd comm q, qinv inv q, true wf, squash wf, qmul over plus qrng, qadd wf, qmul wf, int inc rationals, rationals wf